(set-logic ALL)
(set-info :status unsat)
(declare-sort $$unsorted 0)
(declare-fun tptp.environment ($$unsorted) Bool)
(declare-fun tptp.e () $$unsorted)
(declare-fun tptp.an_organisation () $$unsorted)
(declare-fun tptp.appear ($$unsorted $$unsorted) $$unsorted)
(declare-fun tptp.number_of_organizations ($$unsorted $$unsorted) $$unsorted)
(declare-fun tptp.zero () $$unsorted)
(declare-fun tptp.greater ($$unsorted $$unsorted) Bool)
(assert (forall ((A $$unsorted)) (or (not (tptp.environment A)) (tptp.greater (tptp.number_of_organizations tptp.e (tptp.appear tptp.an_organisation A)) tptp.zero))))
(declare-fun tptp.sk1 ($$unsorted $$unsorted) $$unsorted)
(declare-fun tptp.subpopulation ($$unsorted $$unsorted $$unsorted) Bool)
(assert (forall ((A $$unsorted) (B $$unsorted)) (or (not (tptp.environment A)) (not (tptp.greater (tptp.number_of_organizations A B) tptp.zero)) (tptp.subpopulation (tptp.sk1 B A) A B))))
(declare-fun tptp.cardinality_at_time ($$unsorted $$unsorted) $$unsorted)
(assert (forall ((A $$unsorted) (B $$unsorted)) (or (not (tptp.environment A)) (not (tptp.greater (tptp.number_of_organizations A B) tptp.zero)) (tptp.greater (tptp.cardinality_at_time (tptp.sk1 B A) B) tptp.zero))))
(declare-fun tptp.in_environment ($$unsorted $$unsorted) Bool)
(declare-fun tptp.efficient_producers () $$unsorted)
(assert (forall ((A $$unsorted) (B $$unsorted)) (or (not (tptp.environment A)) (not (tptp.in_environment A B)) (not (tptp.greater (tptp.appear tptp.efficient_producers A) B)) (not (tptp.greater (tptp.cardinality_at_time tptp.efficient_producers B) tptp.zero)))))
(declare-fun tptp.first_movers () $$unsorted)
(assert (forall ((A $$unsorted) (B $$unsorted)) (or (not (tptp.environment A)) (not (tptp.in_environment A B)) (not (tptp.greater (tptp.appear tptp.first_movers A) B)) (not (tptp.greater (tptp.cardinality_at_time tptp.first_movers B) tptp.zero)))))
(declare-fun tptp.greater_or_equal ($$unsorted $$unsorted) Bool)
(assert (forall ((A $$unsorted)) (or (not (tptp.environment A)) (tptp.greater_or_equal (tptp.appear tptp.first_movers A) (tptp.appear tptp.an_organisation A)))))
(assert (forall ((A $$unsorted) (B $$unsorted) (C $$unsorted)) (or (not (tptp.greater A B)) (not (tptp.greater B C)) (tptp.greater A C))))
(assert (forall ((A $$unsorted) (B $$unsorted)) (or (not (tptp.greater_or_equal A B)) (tptp.greater A B) (= A B))))
(assert (forall ((A $$unsorted) (B $$unsorted)) (or (not (tptp.greater A B)) (tptp.greater_or_equal A B))))
(assert (forall ((A $$unsorted) (B $$unsorted)) (or (not (= A B)) (tptp.greater_or_equal A B))))
(assert (forall ((A $$unsorted) (B $$unsorted) (C $$unsorted)) (or (not (tptp.environment A)) (not (tptp.subpopulation B A C)) (not (tptp.greater (tptp.cardinality_at_time B C) tptp.zero)) (= B tptp.efficient_producers) (= B tptp.first_movers))))
(assert (forall ((A $$unsorted)) (or (not (tptp.environment A)) (tptp.greater (tptp.appear tptp.efficient_producers tptp.e) (tptp.appear tptp.first_movers A)))))
(declare-fun tptp.sk2 () $$unsorted)
(assert (tptp.environment tptp.sk2))
(assert (tptp.in_environment tptp.sk2 (tptp.appear tptp.an_organisation tptp.sk2)))
(assert (not (= (tptp.appear tptp.an_organisation tptp.sk2) (tptp.appear tptp.first_movers tptp.sk2))))
(set-info :filename MGT031-1)
(check-sat)
